Định lý bốn màu (còn gọi là định lý bản đồ bốn màu) phát biểu rằng đối với bất kỳ mặt phẳng nào được chia thành các vùng phân biệt, chẳng hạn như bản đồ hành chính của một quốc gia, chỉ cần dùng tối đa bốn màu để phân biệt các vùng lân cận với nhau. Hai vùng được coi là lân cận nếu như chúng có chung nhau một đoạn đường biên, không tính chung nhau một điểm.Định lý bốn màu là định lý lớn đầu tiên được chứng minh bằng máy vi tính. Tuy nhiên một số nhà toán học không đồng tình với cách chứng minh này, bởi vì con người không thể kiểm chứng trực tiếp được cách chứng minh. Do vậy, muốn tin vào chứng minh này thì người ta phải công nhận sự chính xác của Trình biên dịch và phần cứng máy tính được sử dụng để chạy chương trình chứng minh.